package tableaux.rules;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import kb.RBox;
import kb.TBox;

import tableaux.*;
import tableaux.backjumping.DependencyImp;
import tableaux.backjumping.DependencyImpMax;

import entities.*;
import entities.concept.*;
import entities.role.Role;

/**
 * @version 0.2 <br>
 *          Updated to deal with inverse roles. Given All R.C, first find all
 *          R-successors, second find all inv-R predecessors.
 * @author j55wu
 * 
 */
public class RuleForAll {

	private UniversalConcept nextExp;
	private Completion dc;
	private Branching br;
	private final TBox tb;
	private final RBox rb;
	private boolean transApp = false;

	public RuleForAll(Completion dc) {
		super();
		this.dc = dc;
		this.br = this.dc.getCurrentBranching();
		this.tb = this.dc.getInitTBox();
		this.rb = this.tb.getRoleBox();
	}

	// test if there is at least one individual that has't this label concept
	private void findMatch(Concept filler, Set<Individual> inds) {
		for (Individual nn : inds) {
			if (!nn.getLabels().contains(filler)) {
				targets.add(nn);
			}
		}
		return;
	}

	private static Set<Individual> targets = new HashSet<Individual>();

	public boolean isApplicable(Individual n) {
		for (Concept c : n.getLabels()) {
			if (n.getExpandedLabels().contains(c)) {
				continue;
			}
			if (c instanceof UniversalConcept) {
				UniversalConcept uc = (UniversalConcept) c;
				Concept filler = uc.getFiller();
				if(filler.isTop()){
					//no need to fill TOP for successors
					continue;
				}
				Role r = uc.getRole();
//				if (Completion.universalGuardsInRule) {
//					PConcept rdef = PConcept.newGuardPConcept(r);
//					n.addLabels(rdef);
//					// no dependency sets for this expansion, as DEFs are
//					// independent of
//					// any other concepts
//					if (BranchChanges.getRecordingStatus()) {
//						br.getBranchChanges().addToLabel(n, rdef);
//					}
//				}
				Set<Individual> rcs = n.getChildren(r, dc.getInitTBox());
//				if (rcs == null) {
//					continue;
//				} else 
					if (rcs.size() > 0) {
					this.findMatch(filler, rcs);
				}
				// for inverse predecessors
				Role ir = rb.getInverseRole(r);
				Set<Individual> irps = n.getParents(ir, tb);
//				if (irps == null) {
//					continue;
//				} else 
					if (irps.size() > 0 && !targets.containsAll(irps)) {
					this.findMatch(filler, irps);
				}
				//also, see if this R is a transitive role superrole
				if(rb.isComplexRole(r)){
					Role s = r;
					//first find all R-successors for S
					this.filterAllChildren(n, s, tb, filler);
					// second find all inverse-R predecessors
//					Role is = RBox.getInverseRole(s);
					this.filterAllParents(n, s, tb, filler);
				}
				if (targets.size() > 0 || transTargets.size() > 0) {
					this.nextExp = uc;
					return true;
				}
			}
		}
		return false;
	}

	/*
	 * ensure all r-successors will have the filler in its label
	 */
	public boolean applyRule(Individual n) {
		boolean suc = false;
		// Role r = this.nextExp.getRole();
		Concept filler = this.nextExp.getFiller();
		suc |= this.applyChanges(filler, targets, n);
		if(transApp){
			//also apply the transitive role rule
			suc |= this.applyTransitiveRoleRule(n);
		}
		targets.clear();
		boolean expadd = n.addExpandedLabels(this.nextExp);
		if (expadd && BranchChanges.getRecordingStatus()) {
			br.getBranchChanges().addToExpandedLabel(n, this.nextExp);
		}
		return suc;
	}

	private boolean applyChanges(Concept filler, Set<Individual> inds,
			Individual father) {
		boolean change = false;
		for (Individual nn : inds) {
			// if(!nn.getLabels().contains(filler)){
			boolean added = nn.addLabels(filler);
			if (!added) {
				continue;
			}
			// add dependency set
			if (Completion.DEP_MAX) {
				int i1 = nn.getGeneratedByMax();
				int i2 = DependencyImpMax.getDepOfConcept(father, nextExp);
				DependencyImpMax.addDep(nn, filler, i1 > i2 ? i1 : i2);
			} else {
				Set<Integer> more = new HashSet<Integer>();
				more.addAll(nn.getGeneratedBy());
				more.addAll(DependencyImp.getDepSetOfConcept(father,
						this.nextExp));
				DependencyImp.setDep(nn, filler, more);
			}
			//
			// this successor has been changed, must be added to the queue for
			// expansion
			// if(!this.dc.getIndividualsInQueue().contains(nn)){
			change |= this.dc.addToQueue(nn,
					Completion.InQueueOrder.INQUEUEFIRST);
			if (change && BranchChanges.getRecordingStatus()) {
				// this node is added for this branch only, must be recorded
				br.getBranchChanges().updateQueueInds(nn, 1);
			}
			// }
			if (added & BranchChanges.getRecordingStatus()) {
				br.getBranchChanges().addToLabel(nn, filler);
			}
			// }
		}
		return change;
	}
	
	
	///methods for transitive roles below////
	private Map<Role,  Set<Individual>> transTargets = new HashMap<Role,  Set<Individual>>();
	
	private boolean applyTransitiveRoleRule(Individual n){
		if(this.transTargets.size()<=0){
			return false;
		}
		boolean suc = this.applyTransitiveChanges(this.nextExp.getFiller(), n);
		transTargets.clear();
		return suc;
	}
	

	private boolean applyTransitiveChanges(Concept fil, Individual father) {
		boolean change = false;
		for(Role s:transTargets.keySet()){
			Concept fc = new UniversalConcept(s, fil);
			for(Individual m: transTargets.get(s)){
				boolean added = m.addLabels(fc);
				if (!added) {
					continue;
				}
				// add dependency set
				if (Completion.DEP_MAX) {
					int i1 = m.getGeneratedByMax();
					int i2 = DependencyImpMax.getDepOfConcept(father, nextExp);
					DependencyImpMax.addDep(m, fil, i1 > i2 ? i1 : i2);
				} else {
					Set<Integer> more = new HashSet<Integer>();
					more.addAll(m.getGeneratedBy());
					more.addAll(DependencyImp.getDepSetOfConcept(father,this.nextExp));
					DependencyImp.setDep(m, fil, more);
				}
				change |= this.dc.addToQueue(m, Completion.InQueueOrder.INQUEUEFIRST);
				if (change && BranchChanges.getRecordingStatus()) {
					br.getBranchChanges().updateQueueInds(m, 1);
				}
				if (added & BranchChanges.getRecordingStatus()) {
					br.getBranchChanges().addToLabel(m, fil);
				}
			}
		}

		return change;
	}
	
	private Set<Individual> filterIndividual(Role r, Concept c, Set<Individual> inds){
		Concept fc = new UniversalConcept(r, c);
		Set<Individual> ret = new HashSet<Individual>();
		for(Individual m:inds){
			//m does not have forall S.C
			if(!m.getLabels().contains(fc)){
				ret.add(m);
			}
		}
		return ret;
	}
	
	private void addAsTarget(Role s, Set<Individual> inds){
		Set<Individual> given;
		if(transTargets.containsKey(s)){
			given = transTargets.get(s);
			given.addAll(inds);
		}else{
			given = inds;
			transTargets.put(s, given);
		}
	}
	
	//find R-succesors and deposit them
	public void filterAllChildren(Individual n, Role s, TBox tb, Concept filler) {
		if (n.getChildrenMap() == null) {
			return;
		}
		if(!rb.getSubRolesMap().containsKey(s)){
			//no subroles, then just get all successors of S
			Set<Individual> chi = n.getChildrenMap().get(s);
			if(chi!=null){
				this.addAsTarget(s, this.filterIndividual(s, filler, chi));
			}
			return;
		}
		//get all successors from subroles
		for(Role r:rb.getAllSubRoles(s)){
			if (n.getChildrenMap().containsKey(r)){
				Set<Individual> chi = n.getChildrenMap().get(r);
				if(chi!=null){
					this.addAsTarget(r, this.filterIndividual(r, filler, chi));
				}
			}
			
		}
		return;
	}

	//find inv-R parents and filter them using all S-.C
	public void filterAllParents(Individual n, Role s, TBox tb, Concept filler) {
		if (n.getParentsMap() == null) {
			return;
		}
		Role is = tb.getRoleBox().getInverseRole(s);
		if(!rb.getSubRolesMap().containsKey(is)){
			//no subroles, then just get all parents of S
			Set<Individual> chi = n.getParentsMap().get(is);
			if(chi!=null){
				transApp = true;
				this.addAsTarget(s, this.filterIndividual(s, filler, chi));
			}
			return;
		}
		//get all successors from subroles
		for(Role ir:rb.getAllSubRoles(is)){
			if (n.getParentsMap().containsKey(ir)){
				Set<Individual> chi = n.getParentsMap().get(ir);
				Role r = tb.getRoleBox().getInverseRole(ir);
				if(chi!=null){
					transApp = true;
					this.addAsTarget(r, this.filterIndividual(r, filler, chi));
				}
			}
			
		}
		return;
	}
	

}
